E:Type, pred?:(E(E+Unit)), a, b, e:E.
SWellFounded(first(y) & x = pred(y)  E)
 (a before b  eventlist(pred?;e)
 (
 ((a ((x,y. first(y) & x = pred(y)  E)^*) e)
 (& (b ((x,y. first(y) & x = pred(y)  E)^*) e)
 (& (a x,y. first(y) & x = pred(y)  E^+ b)) 

latex

Definitions

x:A. B(x), P  Q, A & B, eventlist(pred?;e), P & Q, x f y, t  T, x,y. t(x;y), Prop, x. t(x), Y, if b t else f fi, true, false, P  Q, P  Q, P  Q, A, R^*, x:A. B(x), , rel_exp(T;R;n), AB, False, i=j, R^+, SQType(T), {T}, Unit, x(s1,s2), WellFnd{i}(A;x,y.R(x;y)), , x(s), Dec(P), SWellFounded(R(x;y)), , , S  T

Lemmas

strongwf-implies, not wf, assert wf, first wf, pred wf, iff wf, l before wf, eventlist wf, rel star wf, rel plus wf, bool wf, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot, strongwellfounded wf, unit wf, cons before, or functionality wrt iff, l member wf, false wf, nil before, decidable false, nil member, rel plus strongwellfounded, iff functionality wrt iff, append wf, l before append iff, le wf, rel exp add, rel exp wf, member singleton, member eventlist, nat plus inc, decidable int equal, nat wf, nat plus wf, nat plus properties, eq int wf, assert of eq int, not functionality wrt iff, rel exp iff